/LMAR=0/XLINE=4/FONT#0=BASL30/FONT#1=BASB30/FONT#5=ASI30[LSP,JRA]/FONT#2=ASI30[LSP,JRA]/FONT#3=SUB/FONT#4=SET1/FONT#6=GRK30/FONT#7=SUP/FONT#8=SPEC[LSP,JRA]/FONT#9=BUCK75/FONT#10=GRFX25[LSP,JRA]/FONT#11=METSB/FONT#12=NGB30/FONT#13=GERM35/FONT#14=MG[LSP,JRA]/FONT#15=GRFX35
␈↓ α←␈↓␈↓␈↓ 	≡CONTENTS     i␈↓

␈↓"β␈↓ α←␈↓↓␈↓ ∧aT A B L E   O F   C O N T E N T S



␈↓"β␈↓ α←␈↓␈↓↓PREFACE␈↓ 
Ei␈↓

␈↓"β␈↓ α←␈↓␈↓↓CHAPTER␈↓ 	|PAGE␈↓


␈↓"β␈↓ α←␈↓␈↓ ββ1␈↓ β3SYMBOLIC EXPRESSIONS␈↓ 
@1

␈↓"β␈↓ α←␈↓␈↓ βc1.1␈↓ ∧+Introduction␈↓ ¬G .  .  .  .  .  .  .  .  .  .  .  .  .  .  .  .  .  .  .  .  .  .  . ␈↓ 
6 1


␈↓"β␈↓ α←␈↓␈↓↓INDEX␈↓ 
A7␈↓
␈↓ α←␈↓␈↓1.␈↓ λ⊃Symbolic expressions     1␈↓




␈↓"β␈↓ α←␈↓␈↓ 	"␈↓↓CHAPTER 1␈↓




␈↓"β␈↓ α←␈↓␈↓	Symbolic Expressions␈↓














␈↓"β␈↓ α←␈↓␈↓ ¬h␈↓↓1.1  Introduction␈↓

␈↓"β␈↓ α←␈↓This␈α∩book␈α⊃is␈α∩a␈α∩study␈α⊃of␈α∩data␈α∩structures␈α⊃and␈α∩programming␈α∩languages;␈α⊃in
␈↓ α←␈↓particular␈α∃it␈α∀is␈α∃a␈α∃study␈α∀of␈α∃data␈α∀structures␈α∃and␈α∃programming␈α∀languages
␈↓ α←␈↓centered␈αaround␈αthe␈αlanguage␈αLISP.␈↓π 1␈↓␈αWe␈αwill␈αstudy␈αmany␈αof␈αthe␈αformal␈α
and
␈↓ α←␈↓theoretical␈αaspects␈αof␈αlanguages␈αand␈αdata␈αstructures␈αas␈αwell␈αas␈αexamining␈αthe
␈↓ α←␈↓practical␈α∩applications␈α∩of␈α∩data␈α∩structures.␈α∪We␈α∩will␈α∩show␈α∩that␈α∩this␈α∪area␈α∩of
␈↓ α←␈↓computer␈αscience␈αis␈αa␈αdiscipline␈αof␈αimportance␈αand␈αbeauty,␈αworthy␈α
of␈αcareful
␈↓ α←␈↓study.␈α⊃ How␈α∩are␈α⊃we␈α⊃to␈α∩proceed?␈↓π 2␈↓␈α⊃We␈α⊃must␈α∩not␈α⊃pursue␈α⊃theory␈α∩and␈α⊃rigor
␈↓ α←␈↓without␈α→proper␈α→regard␈α→for␈α→practice.␈α~Our␈α→study␈α→is␈α→not␈α→that␈α~of␈α→pure
␈↓ α←␈↓mathematics;␈α⊃our␈α∩results␈α⊃will␈α⊃have␈α∩applications␈α⊃in␈α∩everyday␈α⊃programming
␈↓ α←␈↓practice.
␈↓"β␈↓ α←␈↓␈↓ β'Number␈α∃theory␈α∃studies␈α∃properties␈α∃of␈α∃a␈α∃certain␈α∃class␈α∃of␈α∃operations
␈↓ α←␈↓definable␈α
over␈αthe␈α
set␈α
␈↓N␈↓␈αof␈α
non-negative␈α
integers␈αalso␈α
called␈αnatural␈α
numbers.
␈↓ α←␈↓A␈αvery␈αformal␈αpresentation␈αmight␈αbegin␈αwith␈αa␈αconstruction␈αof␈α␈↓N␈↓␈αfrom␈αmore

␈↓"β␈↓ α←␈↓________________
␈↓"β␈↓ α←␈↓␈↓ β'␈↓π 1␈↓However,␈αthis␈αis␈α
not␈αa␈αmanual␈αto␈α
help␈αyou␈αbecome␈αa␈α
proficient␈αLISP
␈↓ α←␈↓coder.
␈↓"β␈↓ α←␈↓␈↓ β'␈↓π 2␈↓How␈α
do␈α
we␈α
introduce␈α
rigor␈α
into␈α
a␈α
field␈α
whose␈α
countenance␈α
is␈α
as␈α␈↓αad␈α
hoc␈↓
␈↓ α←␈↓and␈αdiverse␈αas␈αthat␈αof␈αprogramming?␈αWe␈αmust␈αbear␈αin␈αmind␈αthat␈αthe␈αresults
␈↓ α←␈↓of our studies are to have practical applications.
␈↓ α←␈↓␈↓2  Symbolic expressions␈↓ 
(1.1␈↓

␈↓"β␈↓ α←␈↓primitive␈α
notions,␈α
but␈α
it␈α
is␈α∞usually␈α
assumed␈α
that␈α
the␈α
reader␈α
is␈α∞familiar␈α
with
␈↓ α←␈↓the␈α∞fundamental␈α∞properties␈α∞of␈α∞␈↓N␈↓.␈α∞ In␈α∞either␈α∞case␈α∞the␈α∞next␈α∞step␈α∞would␈α∂be␈α∞to
␈↓ α←␈↓define the class of operations which we would allow on our domain.
␈↓"β␈↓ α←␈↓␈↓ β'For␈αmost␈αpeople␈αand␈αmost␈αpurposes,␈αthe␈αfollowing␈αcharacterization␈αof␈αa
␈↓ α←␈↓natural number is satisfactory:

␈↓"β␈↓ α←␈↓␈↓↓I␈↓␈↓ β∂A natural number is a sequence of decimal digits.

␈↓"β␈↓ α←␈↓The␈α
definition␈α
assumes␈α
the␈α
terminology␈α
of␈α
"sequence",␈α
"decimal"␈α∞and␈α
"digit"
␈↓ α←␈↓are␈α∂known.␈α⊂If␈α∂any␈α⊂of␈α∂these␈α⊂terms␈α∂are␈α⊂␈↓¬not␈↓␈α∂understood,␈α⊂they␈α∂can␈α⊂be␈α∂further
␈↓ α←␈↓elaborated.␈α⊗However,␈α↔this␈α⊗process␈α⊗of␈α↔explanation␈α⊗and␈α↔description␈α⊗must
␈↓ α←␈↓terminate.␈α≤We␈α≠must␈α≤assume␈α≠that␈α≤some␈α≠concepts␈α≤require␈α≤no␈α≠further
␈↓ α←␈↓elaboration.␈α→The␈α→current␈α→definition␈α→suffers␈α→from␈α→a␈α→different␈α→kind␈α→of
␈↓ α←␈↓inadequacy.␈αIt␈α
fails␈αto␈α
illuminate␈αthe␈α
relationships␈αbetween␈α
natural␈αnumbers.
␈↓ α←␈↓The␈α"meaning"␈α
of␈αthe␈α
natural␈αnumbers␈α
is␈αmissing.␈α
It␈αis␈α
like␈αgiving␈α
a␈αperson
␈↓ α←␈↓an␈α⊗alphabet␈α∃and␈α⊗rules␈α∃for␈α⊗forming␈α∃syntactically␈α⊗correct␈α∃words␈α⊗but␈α∃not
␈↓ α←␈↓supplying a dictionary which relates these words to the person's vocabulary.
␈↓"β␈↓ α←␈↓␈↓ β'If␈α!pressed␈α!for␈α!details␈α"we␈α!might␈α!attempt␈α!a␈α"more␈α!elaborate
␈↓ α←␈↓characterization like the following:

␈↓"β␈↓ α←␈↓␈↓ β≠␈↓↓1.␈↓ ␈↓αzero␈↓ is an element of ␈↓N␈↓.
␈↓"β␈↓ α←␈↓␈↓↓II␈↓   ␈↓↓2.␈↓ If ␈↓αn␈↓ is in ␈↓N␈↓ then the ␈↓αsuccessor␈↓ of ␈↓αn␈↓ is in ␈↓N␈↓.
␈↓"β␈↓ α←␈↓␈↓ β≠␈↓↓3.␈↓␈α
The␈α
only␈α
elements␈α
of␈α␈↓N␈↓␈α
are␈α
those␈α
created␈α
by␈α
finitely␈αmany␈α
applications
␈↓ α←␈↓␈↓ β≠of rules ␈↓↓1␈↓ and ␈↓↓2␈↓.

␈↓"β␈↓ α←␈↓␈↓ β'We␈α∂can␈α∂define␈α∂␈↓αsuccessor␈↓␈α∂as␈α∂a␈α∂specific␈α∂mapping,␈α∂␈↓↓S␈↓,␈α∂which␈α∂creates␈α∂new
␈↓ α←␈↓elements␈αsubject␈αto␈αthe␈αrules␈αthat␈αtwo␈αelements,␈α␈↓αx␈↓␈αand␈α␈↓αy␈↓␈αare␈αequal␈αjust␈αin␈αthe
␈↓ α←␈↓case␈α∞that␈α∞␈↓↓S␈↓α(x)␈↓␈α∞equals␈α
␈↓↓S␈↓α(y)␈↓;␈α∞and␈α∞␈↓↓S␈↓α(x)␈↓␈α∞is␈α∞different␈α
from␈α∞␈↓αx␈↓,␈α∞for␈α∞any␈α∞element␈α
␈↓αx␈↓.
␈↓ α←␈↓We␈α
select␈α
a␈α∞distinguished␈α
element,␈α
␈↓α0␈↓,␈α
as␈α∞a␈α
notation␈α
for␈α
␈↓αzero␈↓;␈α∞and␈α
abbreviate
␈↓ α←␈↓␈↓↓S␈↓α(0)␈↓ as ␈↓α1␈↓, and abbreviate ␈↓↓S␈↓α(␈↓↓S␈↓α(0))␈↓ as ␈↓α2␈↓ etc. in the usual manner.
␈↓"β␈↓ α←␈↓␈↓ β'Given␈α∪a␈α∪choice␈α∪between␈α∪the␈α∪two␈α∪previous␈α∪definitions,␈α∪␈↓↓I␈↓␈α∪and␈α∪␈↓↓II␈↓,␈α∩it
␈↓ α←␈↓appears␈α
that␈α
␈↓↓II␈↓␈α
is␈α
more␈α
precise.␈α
 Much␈α
less␈α
is␈α
left␈α
to␈α
the␈α
imagination;␈α
given
␈↓ α←␈↓␈↓αzero␈↓␈α∩and␈α⊃a␈α∩definition␈α∩of␈α⊃␈↓αsuccessor␈↓␈α∩the␈α⊃definition␈α∩will␈α∩act␈α⊃as␈α∩a␈α∩recipe␈α⊃for
␈↓ α←␈↓producing␈α∩elements␈α∪of␈α∩␈↓N␈↓.␈α∪This␈α∩style␈α∪of␈α∩definition␈α∪is␈α∩called␈α∪an␈α∩inductive
␈↓ α←␈↓definition or generative definition.
␈↓ α←␈↓␈↓1.1␈↓ λ|Introduction     3␈↓

␈↓"β␈↓ α←␈↓␈↓ β'The␈αbasic␈αcontent␈αof␈αan␈αinductive␈αdefinition␈αof␈αa␈αset␈αof␈αobjects␈αconsists
␈↓ α←␈↓of three parts:

␈↓"β␈↓ α←␈↓␈↓ βW(1)␈αA␈αdescription␈αof␈αan␈αinitial␈αset␈αof␈αobjects;␈αthe␈αelements␈αof␈αthis␈αset
␈↓ α←␈↓␈↓ βWare␈αthe␈αinitial␈αelements␈αof␈αthe␈αset␈αwe␈αare␈αdescribing␈αin␈αthe␈αinductive
␈↓ α←␈↓␈↓ βWdefinition.
␈↓"β␈↓ α←␈↓␈↓↓IND␈↓
␈↓"β␈↓ α←␈↓␈↓ βW(2)␈α∞Given␈α∂the␈α∞description␈α∞of␈α∂some␈α∞existing␈α∞elements␈α∂in␈α∞the␈α∂set,␈α∞we
␈↓ α←␈↓␈↓ βWare given a means of constructing more elements.
␈↓"	␈↓ α←␈↓␈↓ βW(3)␈αA␈α
termination␈αclause,␈α
saying␈αthat␈αthe␈α
only␈αelements␈α
in␈αthe␈αset␈α
are
␈↓ α←␈↓␈↓ βWthose which gained admittance by either (1) or (2).

␈↓"β␈↓ α←␈↓Notice␈αthat␈αour␈αdefinition␈αof␈α␈↓N␈↓,␈αin␈αterms␈αof␈α␈↓αzero␈↓␈αand␈α␈↓αsuccessor␈↓,␈αis␈αan␈αinstance
␈↓ α←␈↓of␈α␈↓↓IND␈↓:␈αwe␈αare␈αdefining␈αthe␈αset␈αof␈αnatural␈αnumbers:␈α␈↓αzero␈↓␈αis␈αinitially␈αincluded
␈↓ α←␈↓in␈αthe␈αset;␈αthen␈αapplying␈αthe␈αsecond␈αphrase␈αof␈αthe␈αdefinition␈αwe␈αcan␈αsay␈αthat
␈↓ α←␈↓␈↓αone␈↓ is in the set since ␈↓αone␈↓ is the successor of ␈↓αzero␈↓.
␈↓"β␈↓ α←␈↓␈↓ β'We␈α∃can␈α∃recast␈α∀the␈α∃positional␈α∃notation␈α∀description␈α∃as␈α∃an␈α∀inductive
␈↓ α←␈↓definition.

␈↓"λ␈↓ α←␈↓␈↓↓1.␈↓  A digit is a numeral.
␈↓"	␈↓ α←␈↓␈↓↓2.␈↓  If ␈↓αn␈↓ is a numeral then ␈↓αn␈↓ followed by a digit is a numeral.
␈↓"	␈↓ α←␈↓␈↓↓3.␈↓  The␈α∂only␈α∂numerals␈α∞are␈α∂those␈α∂created␈α∂by␈α∞finitely␈α∂many␈α∂applications␈α∂of␈α∞␈↓↓1␈↓
␈↓ α←␈↓␈↓ β∂and ␈↓↓2␈↓.

␈↓"β␈↓ α←␈↓In words, "a numeral is a digit, or a numeral followed by a digit".
␈↓"β␈↓ α←␈↓␈↓ β'In␈α∞this␈α
application␈α∞of␈α
␈↓↓IND␈↓,␈α∞the␈α∞initial␈α
set␈α∞has␈α
more␈α∞than␈α∞one␈α
element;
␈↓ α←␈↓namely␈α
the␈αten␈α
decimal␈α
digits.␈α Again,␈α
we␈α
assume␈αthat␈α
the␈α
questioner␈αknows
␈↓ α←␈↓what␈α
"digit"␈α
means.␈α
 This␈α
is␈α
a␈α
characteristic␈α
of␈α
all␈α
definitions:␈α
we␈α∞must␈α
stop
␈↓ α←␈↓␈↓¬somewhere␈↓␈α∞in␈α∞our␈α∞explication.␈α∞Notice␈α∞too␈α∞that␈α∞we␈α∞assume␈α∞that␈α∞"followed␈α
by"
␈↓ α←␈↓means juxtaposition.
␈↓"β␈↓ α←␈↓␈↓ β'Inductive␈αdefinitions␈αhave␈αbeen␈αthe␈αprovince␈αof␈αmathematics␈α
for␈αmany
␈↓ α←␈↓years;␈α
however,␈αcomputer␈α
science␈αhas␈α
developed␈α
a␈αstyle␈α
of␈αsyntax␈α
specification
␈↓ α←␈↓called␈α
BNF␈α(Backus-Naur␈α
Form)␈αequations␈α
which␈αhas␈α
the␈αsame␈α
intent␈αas␈α
that
␈↓ α←␈↓of␈α↔inductive␈α⊗definitions.␈α↔ Here␈α⊗is␈α↔the␈α⊗previous␈α↔inductive␈α↔definition␈α⊗of
␈↓ α←␈↓"numeral" as a set of BNF equations:
␈↓"∀␈↓ α←␈↓<numeral>␈↓ ∧π::= <digit>
␈↓"	␈↓ α←␈↓<numeral>␈↓ ∧π::= <numeral><digit>
␈↓"β␈↓ α←␈↓As an abbreviation, the  two BNF equations may also be written:
␈↓"β␈↓ α←␈↓<numeral>␈↓ ∧π::= <digit> | <numeral><digit>.
␈↓"∀␈↓ α←␈↓A␈αcomparison␈αbetween␈αthe␈αBNF␈αand␈αthe␈αinductive␈αdescriptions␈αof␈α"numeral"
␈↓ α←␈↓should␈α∀clarify␈α∪much␈α∀of␈α∪the␈α∀notation,␈α∀but␈α∪we␈α∀will␈α∪give␈α∀a␈α∀more␈α∪detailed
␈↓ α←␈↓analysis.␈α∞ The␈α∞symbol␈α∞"::="␈α∂may␈α∞be␈α∞read␈α∞"is␈α∞a",␈α∂the␈α∞symbol␈α∞"|"␈α∞may␈α∂be␈α∞read
␈↓ α←␈↓␈↓4  Symbolic expressions␈↓ 
(1.1␈↓

␈↓"β␈↓ α←␈↓"or".␈α↔ The␈α↔character␈α↔strings␈α↔beginning␈α↔with␈α↔"<"␈α↔and␈α↔ending␈α_with␈α↔">"
␈↓ α←␈↓correspond␈α
to␈α"numeral"␈α
and␈α
"digit"␈αin␈α
␈↓↓1␈↓␈α
and␈α␈↓↓2␈↓;␈α
by␈α
convention,␈αcomponents␈α
of
␈↓ α←␈↓BNF␈α⊃equations␈α⊃which␈α⊃␈↓¬describe␈↓␈α⊃elements␈α⊃are␈α⊃enclosed␈α⊃in␈α⊃"<"␈α⊃and␈α⊃">";␈α⊃and
␈↓ α←␈↓elements␈α
which␈α
are␈αgiven␈α
␈↓¬explicitly␈↓␈α
are␈α
written␈αwithout␈α
the␈α
"<␈α
>"␈αfence.␈α
 Thus
␈↓ α←␈↓"<digit>"␈α⊂is␈α⊂not␈α∂a␈α⊂numeral␈α⊂but␈α∂is␈α⊂a␈α⊂description;␈α∂to␈α⊂make␈α⊂the␈α⊂definition␈α∂of
␈↓ α←␈↓<numeral> complete we should include an equation like:
␈↓"∀␈↓ α←␈↓<digit>␈↓ ∧π:: = ␈↓α0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9␈↓
␈↓"∀␈↓ α←␈↓Juxtaposition␈α
of␈α
objects␈α
implies␈α
concatenation␈α
of␈α
the␈α
syntactic␈α
objects.␈αThus
␈↓ α←␈↓"89" is an instance of "<numeral><digit>".
␈↓"β␈↓ α←␈↓␈↓ β'We␈αhave␈αalso␈αintroduced␈αthe␈αdifference␈αbetween␈αan␈αabstract␈αobject␈αand
␈↓ α←␈↓a␈α∂representation␈α∞for␈α∂that␈α∂object.␈α∞ This␈α∂distinction␈α∂has␈α∞been␈α∂well␈α∂studied␈α∞in
␈↓ α←␈↓philosophy␈α∪and␈α∪mathematics,␈α∪and␈α∪we␈α∀will␈α∪see␈α∪that␈α∪this␈α∪idea␈α∀has␈α∪strong
␈↓ α←␈↓consequences␈α∞for␈α∞the␈α
field␈α∞of␈α∞programming␈α
and␈α∞computer␈α∞science.␈α
 Abstract
␈↓ α←␈↓objects and their representations will play crucial roles in this text.
␈↓"β␈↓ α←␈↓With this introduction, here is ␈↓αcomplis␈↓ and friends:
␈↓"∀␈↓ α←␈↓␈↓αcomplis <= λ[[u;off;vpl] complis␈↓λ'␈↓α[u;off;off;vpl;();();();1]␈↓
␈↓"∀␈↓ α←␈↓αcomplis␈↓λ'␈↓α <= λ[[u;org;off;vpl;triv;cmplx;pop;ac]
␈↓"β␈↓ α←␈↓α␈↓ ∧∪[null[u] →␈↓ ¬↔[null[cmplx] → triv;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔ ␈↓
t␈↓α → append␈↓ ε3[rest[cmplx];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ε3 list[mkmove[mem[first[pop]];1]];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ε3 rest[pop];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ε3 triv]];
␈↓"	␈↓ α←␈↓α␈↓ ∧∪ isconst[first[u]] → complis␈↓λ'␈↓α[␈↓ ε{rest[u];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ε{org;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ε{off;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ε{vpl;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ε{concat[mkconst[ac;first[u]];triv];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ε{cmplx;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ε{pop;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ε{add1[ac]];
␈↓"	␈↓ α←␈↓α␈↓ ∧∪ isvar[first[u]] → complis␈↓λ'␈↓α[␈↓ εcrest[u];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ εcorg;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ εcoff;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ εcvpl;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ εcconcat[␈↓ π7mkvar[␈↓ λac;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ εc␈↓ π7␈↓ λloc[first[u];off;vpl]];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ εc␈↓ π7triv];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ εccmplx;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ εcpop;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ εcadd1[ac]];
␈↓ α←␈↓␈↓1.1␈↓ λ|Introduction     5␈↓

␈↓"	␈↓ α←␈↓α␈↓ ∧∪ iscarcdr[first[u]] → complis␈↓λ'␈↓α[␈↓ ππrest[u];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππorg;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππoff;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππvpl;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππappend[␈↓ πsreverse[compcarcdr[␈↓ 	cac;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππ␈↓ πs␈↓ 	c first[u]
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππ␈↓ πs␈↓ 	c off;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππ␈↓ πs␈↓ 	c vpl]];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππ␈↓ πstriv];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππcmplx;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππpop;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬↔␈↓ ππadd1[ac]];
␈↓"	␈↓ α←␈↓α␈↓ ∧∪ iscond[first[u] → complis␈↓λ'␈↓α[␈↓ εorest[u];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εoorg;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εosub1[off];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εovpl;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εotriv;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εoappend[␈↓ π[cmplx;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εo␈↓ π[concat[␈↓ λ/mkpush[1];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εo␈↓ π[␈↓ λ/comcond[␈↓ 	≠args␈↓βc␈↓α[␈↓ 	cfirst[u]]
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εo␈↓ π[␈↓ λ/␈↓ 	≠gensym[];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εo␈↓ π[␈↓ λ/␈↓ 	≠off;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εo␈↓ π[␈↓ λ/␈↓ 	≠vpl]]];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εoconcat[mkpop[ac];pop];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬#␈↓ εoadd1[ac]];
␈↓"	␈↓ α←␈↓α␈↓ ∧∪ ␈↓
t␈↓α → complis␈↓λ'␈↓α[␈↓ ¬Grest[u];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬Gorg;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬Gsub1[off];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬Gvpl;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬Gtriv;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬Gappend[␈↓ ε3cmplx;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬G␈↓ ε3concat[␈↓ ππmkpush[1];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬G␈↓ ε3␈↓ ππλ[[z] compapply[␈↓ λ←func[first[u]];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬G␈↓ ε3␈↓ ππ␈↓ λ←complis[␈↓ 	Kz;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬G␈↓ ε3␈↓ ππ␈↓ λ←␈↓ 	Koff;
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬G␈↓ ε3␈↓ ππ␈↓ λ←␈↓ 	Kvpl];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬G␈↓ ε3␈↓ ππ␈↓ λ←length[z]]]
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬G␈↓ ε3␈↓ ππ [arglist[first[u]] ]];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬Gconcat[mkpop[ac];pop];
␈↓"β␈↓ α←␈↓α␈↓ ∧∪␈↓ ¬Gadd1[ac]]]
␈↓"→␈↓ α←␈↓αmkmove <= λ[[ac;loc][eq[ac;loc] → (); ␈↓
t␈↓α → list[MOVE;ac;loc]]]
␈↓ α←␈↓␈↓6  Symbolic expressions␈↓ 
(1.1␈↓

␈↓"∀␈↓ α←␈↓αcompcarcdr <= λ[[ac;exp;off;vpl]
␈↓"β␈↓ α←␈↓α␈↓ βK␈↓ ∧7[isvar[arg[exp]] → list[mkcarcdr[␈↓ π[func[exp];
␈↓"β␈↓ α←␈↓α␈↓ βK␈↓ ∧7␈↓ ¬G␈↓ π[ac;
␈↓"β␈↓ α←␈↓α␈↓ βK␈↓ ∧7␈↓ ¬G␈↓ π[loc[arg[exp];off;vpl]]]
␈↓"β␈↓ α←␈↓α␈↓ βK␈↓ ∧7␈↓
t␈↓α → concat[␈↓ ¬Gmkcarcdr_ac[func[exp];ac;ac];
␈↓"β␈↓ α←␈↓α␈↓ βK␈↓ ∧7␈↓ ¬Gcompcarcdr[ac;arg[exp];off;vpl]]]]
␈↓"∀␈↓ α←␈↓αiscarcdr <=λ[[u]␈↓ ∧7[iscar[u] →iscarcdr[arg[u]]
␈↓"β␈↓ α←␈↓α␈↓ βK␈↓ ∧7 iscdr[u] →iscarcdr[arg[u]]
␈↓"β␈↓ α←␈↓α␈↓ βK␈↓ ∧7 atom[u] → or[isvar[u];isconst[u]];
␈↓"β␈↓ α←␈↓α␈↓ βK␈↓ ∧7 ␈↓
t␈↓α → ␈↓
f␈↓α ]]
␈↓"∀␈↓ α←␈↓αiscar <= λ[[x] eq[func[x];CAR]]
␈↓"	␈↓ α←␈↓αiscdr <= λ[[x] eq[func[x];CDR]]
␈↓"	␈↓ α←␈↓αmkcarcdr <=λ[[carcdr;ac;loc] list[carcdr;ac;loc]]
␈↓ α←␈↓␈↓␈↓ 	KINDEX     7␈↓









␈↓ α←␈↓␈↓	Index␈↓












␈↓ α←␈↓generative definition   2
␈↓ α←␈↓inductive definition   2